Micron Document
<!DOCTYPE html>
<html class="client-nojs vector-feature-night-mode-disabled vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-sticky-header-enabled" lang="en" dir="ltr"><head>
<meta charset="UTF-8">
<title>Two-element Boolean algebra</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="canonical" href="https://en.wikipedia.org/wiki/Two-element_Boolean_algebra"> <link href="./mw/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/ext.math.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/user.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link rel="stylesheet" type="text/css" href="./mw/site.styles.css">
<link rel="stylesheet" type="text/css" href="./mw/noscript.css">
<link rel="stylesheet" type="text/css" href="./footer.css">
<link rel="stylesheet" type="text/css" href="./vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Two-element_Boolean_algebra rootpage-Two-element_Boolean_algebra skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading">
<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Two-element Boolean algebra</span></span>
</h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">
<p>In <a href="Mathematics" title="Mathematics">mathematics</a> and <a href="Abstract_algebra" title="Abstract algebra">abstract algebra</a>, the <b>two-element Boolean algebra</b> is the <a href="Boolean_algebra_(structure)" title="Boolean algebra (structure)">Boolean algebra</a> whose <i>underlying set</i> (or <a href="Universe_(mathematics)" title="Universe (mathematics)">universe</a> or <i>carrier</i>) <i>B</i> is the <a href="Boolean_domain" title="Boolean domain">Boolean domain</a>. The elements of the Boolean domain are 1 and 0 by convention, so that <i>B</i>&nbsp;=&nbsp;{0,&nbsp;1}. <a href="Paul_Halmos" title="Paul Halmos">Paul Halmos</a>'s name for this algebra "<b>2</b>" has some following in the literature, and will be employed here.
</p>
<meta property="mw:PageProp/toc">
<div class="mw-heading mw-heading2"><h2 id="Definition">Definition</h2></div>
<p><i>B</i> is a <a href="Partial_order" class="mw-redirect" title="Partial order">partially ordered set</a> and the elements of <i>B</i> are also its <a href="Bounded_set#Boundedness_in_order_theory" title="Bounded set">bounds</a>.
</p><p>An <a href="Operation_(mathematics)" title="Operation (mathematics)">operation</a> of <a href="Arity" title="Arity">arity</a> <i>n</i> is a <a href="Map_(mathematics)" title="Map (mathematics)">mapping</a> from <i>B</i><sup>n</sup> to <i>B</i>. Boolean algebra consists of two <a href="Binary_operation" title="Binary operation">binary operations</a> and <a href="Unary_operation" title="Unary operation">unary</a> <a href="Complement_(order_theory)" class="mw-redirect" title="Complement (order theory)">complementation</a>. The binary operations have been named and notated in various ways. Here they are called 'sum' and 'product', and notated by infix '+' and '∙', respectively. Sum and product <a href="Commutativity" class="mw-redirect" title="Commutativity">commute</a> and <a href="Associativity" class="mw-redirect" title="Associativity">associate</a>, as in the usual <a href="Elementary_algebra" title="Elementary algebra">algebra of real numbers</a>. As for the <a href="Order_of_operations" title="Order of operations">order of operations</a>, brackets are decisive if present. Otherwise '∙' precedes '+'. Hence <span class="texhtml"><i>A</i> ∙ <i>B</i> + <i>C</i></span> is parsed as <span class="texhtml">(<i>A</i> ∙ <i>B</i>) + <i>C</i></span> and not as <span class="texhtml"><i>A</i> ∙ (<i>B</i> + <i>C)</i></span>. <a href="Boolean_algebra_(logic)" class="mw-redirect" title="Boolean algebra (logic)">Complementation</a> is denoted by writing an overbar over its argument. The numerical analog of the complement of <span class="texhtml mvar" style="font-style:italic;">X</span> is <span class="texhtml">1 − <i>X</i></span>. In the language of <a href="Universal_algebra" title="Universal algebra">universal algebra</a>, a Boolean algebra is a <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle B,+,}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">⟨<!-- ⟨ --></mo>
<mi>B</mi>
<mo>,</mo>
<mo>+</mo>
<mo>,</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \langle B,+,}</annotation>
</semantics>
</math></span><img src="./498f38df7f951e3e71414ba5b353088287ba7dd5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.158ex; height:2.843ex;" alt="{\displaystyle \langle B,+,}" loading="lazy"></span>∙<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ,{\overline {..}},1,0\rangle }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo>,</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mo>.</mo>
<mo>.</mo>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>,</mo>
<mn>1</mn>
<mo>,</mo>
<mn>0</mn>
<mo fence="false" stretchy="false">⟩<!-- ⟩ --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle ,{\overline {..}},1,0\rangle }</annotation>
</semantics>
</math></span><img src="./4f2817bbb30e42c6486437515ef64e60a0d0b780.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.127ex; height:2.843ex;" alt="{\displaystyle ,{\overline {..}},1,0\rangle }" loading="lazy"></span> <a href="Algebraic_structure" title="Algebraic structure">algebra</a> of <a href="Arity" title="Arity">type</a> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle 2,2,1,0,0\rangle }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">⟨<!-- ⟨ --></mo>
<mn>2</mn>
<mo>,</mo>
<mn>2</mn>
<mo>,</mo>
<mn>1</mn>
<mo>,</mo>
<mn>0</mn>
<mo>,</mo>
<mn>0</mn>
<mo fence="false" stretchy="false">⟩<!-- ⟩ --></mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \langle 2,2,1,0,0\rangle }</annotation>
</semantics>
</math></span><img src="./3b8fad55cdb4ed42d645feba54623c8fd96cd00a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.757ex; height:2.843ex;" alt="{\displaystyle \langle 2,2,1,0,0\rangle }" loading="lazy"></span>.
</p><p>Either <a href="One-to-one_correspondence" class="mw-redirect" title="One-to-one correspondence">one-to-one correspondence</a> between {0,1} and {<i>True</i>,<i>False</i>} yields classical <a href="Bivalent_logic" class="mw-redirect" title="Bivalent logic">bivalent logic</a> in equational form, with complementation read as <a href="Logical_NOT" class="mw-redirect" title="Logical NOT">NOT</a>. If 1 is read as <i>True</i>, '+' is read as <a href="Logical_OR" class="mw-redirect" title="Logical OR">OR</a>, and '∙' as <a href="Logical_AND" class="mw-redirect" title="Logical AND">AND</a>, and vice versa if 1 is read as <i>False</i>. These two operations define a commutative <a href="Semiring" title="Semiring">semiring</a>, known as the <a href="Boolean_semiring" class="mw-redirect" title="Boolean semiring">Boolean semiring</a>.
</p>
<div class="mw-heading mw-heading2"><h2 id="Some_basic_identities">Some basic identities</h2></div>
<p><b>2</b> can be seen as grounded in the following trivial "Boolean" arithmetic:
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}&amp;1+1=1+0=0+1=1\\&amp;0+0=0\\&amp;0\cdot 0=0\cdot 1=1\cdot 0=0\\&amp;1\cdot 1=1\\&amp;{\overline {1}}=0\\&amp;{\overline {0}}=1\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd></mtd>
<mtd>
<mn>1</mn>
<mo>+</mo>
<mn>1</mn>
<mo>=</mo>
<mn>1</mn>
<mo>+</mo>
<mn>0</mn>
<mo>=</mo>
<mn>0</mn>
<mo>+</mo>
<mn>1</mn>
<mo>=</mo>
<mn>1</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mn>0</mn>
<mo>+</mo>
<mn>0</mn>
<mo>=</mo>
<mn>0</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mn>0</mn>
<mo>⋅<!-- ⋅ --></mo>
<mn>0</mn>
<mo>=</mo>
<mn>0</mn>
<mo>⋅<!-- ⋅ --></mo>
<mn>1</mn>
<mo>=</mo>
<mn>1</mn>
<mo>⋅<!-- ⋅ --></mo>
<mn>0</mn>
<mo>=</mo>
<mn>0</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mn>1</mn>
<mo>⋅<!-- ⋅ --></mo>
<mn>1</mn>
<mo>=</mo>
<mn>1</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mn>1</mn>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>=</mo>
<mn>0</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mn>0</mn>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>=</mo>
<mn>1</mn>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}&amp;1+1=1+0=0+1=1\\&amp;0+0=0\\&amp;0\cdot 0=0\cdot 1=1\cdot 0=0\\&amp;1\cdot 1=1\\&amp;{\overline {1}}=0\\&amp;{\overline {0}}=1\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./ad72526fe0d25ae95e745eaa47424c2b029f0024.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -8.838ex; width:26.705ex; height:18.843ex;" alt="{\displaystyle {\begin{aligned}&amp;1+1=1+0=0+1=1\\&amp;0+0=0\\&amp;0\cdot 0=0\cdot 1=1\cdot 0=0\\&amp;1\cdot 1=1\\&amp;{\overline {1}}=0\\&amp;{\overline {0}}=1\end{aligned}}}" loading="lazy"></span></dd></dl>
<p>Note that:
</p>
<ul><li>'+' and '∙' work exactly as in numerical arithmetic, except that 1+1=1. '+' and '∙' are derived by analogy from numerical arithmetic; simply set any nonzero number to 1.</li>
<li>Swapping 0 and 1, and '+' and '∙' preserves truth; this is the essence of the <a href="Duality_(order_theory)" title="Duality (order theory)">duality</a> pervading all Boolean algebras.</li></ul>
<p>This Boolean arithmetic suffices to verify any equation of <b>2</b>, including the axioms, by examining every possible assignment of 0s and 1s to each variable (see <a href="Decision_procedure" class="mw-redirect" title="Decision procedure">decision procedure</a>).
</p><p>The following equations may now be verified:
</p>
<dl><dd><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}&amp;A+A=A\\&amp;A\cdot A=A\\&amp;A+0=A\\&amp;A+1=1\\&amp;A\cdot 0=0\\&amp;{\overline {\overline {A}}}=A\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd></mtd>
<mtd>
<mi>A</mi>
<mo>+</mo>
<mi>A</mi>
<mo>=</mo>
<mi>A</mi>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mi>A</mi>
<mo>=</mo>
<mi>A</mi>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi>A</mi>
<mo>+</mo>
<mn>0</mn>
<mo>=</mo>
<mi>A</mi>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi>A</mi>
<mo>+</mo>
<mn>1</mn>
<mo>=</mo>
<mn>1</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mn>0</mn>
<mo>=</mo>
<mn>0</mn>
</mtd>
</mtr>
<mtr>
<mtd></mtd>
<mtd>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mover>
<mi>A</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>=</mo>
<mi>A</mi>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}&amp;A+A=A\\&amp;A\cdot A=A\\&amp;A+0=A\\&amp;A+1=1\\&amp;A\cdot 0=0\\&amp;{\overline {\overline {A}}}=A\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./fe9ad6a8c26d8de844d92e0d6888e0360c20e626.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -9.005ex; width:11.92ex; height:19.176ex;" alt="{\displaystyle {\begin{aligned}&amp;A+A=A\\&amp;A\cdot A=A\\&amp;A+0=A\\&amp;A+1=1\\&amp;A\cdot 0=0\\&amp;{\overline {\overline {A}}}=A\end{aligned}}}" loading="lazy"></span></dd></dl>
<p>Each of '+' and '∙' <a href="Distributivity" class="mw-redirect" title="Distributivity">distributes</a> over the other:
</p>
<ul><li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \ A\cdot (B+C)=A\cdot B+A\cdot C;}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mtext>&nbsp;</mtext>
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mo stretchy="false">(</mo>
<mi>B</mi>
<mo>+</mo>
<mi>C</mi>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mi>B</mi>
<mo>+</mo>
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mi>C</mi>
<mo>;</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \ A\cdot (B+C)=A\cdot B+A\cdot C;}</annotation>
</semantics>
</math></span><img src="./94740327e18b9599dc226c52f4c91546d8a6725f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:29.143ex; height:2.843ex;" alt="{\displaystyle \ A\cdot (B+C)=A\cdot B+A\cdot C;}" loading="lazy"></span></li>
<li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \ A+(B\cdot C)=(A+B)\cdot (A+C).}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mtext>&nbsp;</mtext>
<mi>A</mi>
<mo>+</mo>
<mo stretchy="false">(</mo>
<mi>B</mi>
<mo>⋅<!-- ⋅ --></mo>
<mi>C</mi>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mo stretchy="false">(</mo>
<mi>A</mi>
<mo>+</mo>
<mi>B</mi>
<mo stretchy="false">)</mo>
<mo>⋅<!-- ⋅ --></mo>
<mo stretchy="false">(</mo>
<mi>A</mi>
<mo>+</mo>
<mi>C</mi>
<mo stretchy="false">)</mo>
<mo>.</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \ A+(B\cdot C)=(A+B)\cdot (A+C).}</annotation>
</semantics>
</math></span><img src="./2b2bf59a2686fd1219359d9629a6719a2de97c4c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.923ex; height:2.843ex;" alt="{\displaystyle \ A+(B\cdot C)=(A+B)\cdot (A+C).}" loading="lazy"></span></li></ul>
<p>That '∙' distributes over '+' agrees with <a href="Elementary_algebra" title="Elementary algebra">elementary algebra</a>, but not '+' over '∙'. For this and other reasons, a sum of products (leading to a <a href="Sheffer_stroke" title="Sheffer stroke">NAND</a> synthesis) is more commonly employed than a product of sums (leading to a <a href="Logical_NOR" title="Logical NOR">NOR</a> synthesis).
</p><p>Each of '+' and '∙' can be defined in terms of the other and complementation:
</p>
<ul><li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\cdot B={\overline {{\overline {A}}+{\overline {B}}}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>A</mi>
<mo>⋅<!-- ⋅ --></mo>
<mi>B</mi>
<mo>=</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>A</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>+</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>B</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle A\cdot B={\overline {{\overline {A}}+{\overline {B}}}}}</annotation>
</semantics>
</math></span><img src="./38ee6a41608a0beab6c7730726307ef55ec62b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:14.977ex; height:4.009ex;" alt="{\displaystyle A\cdot B={\overline {{\overline {A}}+{\overline {B}}}}}" loading="lazy"></span></li>
<li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A+B={\overline {{\overline {A}}\cdot {\overline {B}}}}.}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>A</mi>
<mo>+</mo>
<mi>B</mi>
<mo>=</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>A</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>⋅<!-- ⋅ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>B</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>.</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle A+B={\overline {{\overline {A}}\cdot {\overline {B}}}}.}</annotation>
</semantics>
</math></span><img src="./214d96e46dda4258fe20a50ce44a7685b30d053a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:15.624ex; height:4.009ex;" alt="{\displaystyle A+B={\overline {{\overline {A}}\cdot {\overline {B}}}}.}" loading="lazy"></span></li></ul>
<p>We only need one binary operation, and <a href="Concatenation" title="Concatenation">concatenation</a> suffices to denote it. Hence concatenation and overbar suffice to notate <b>2</b>. This notation is also that of <a href="Willard_Van_Orman_Quine" title="Willard Van Orman Quine">Quine</a>'s Boolean term schemata. Letting (<i>X</i>) denote the complement of <i>X</i> and "()" denote either 0 or 1 yields the <a href="Syntax" title="Syntax">syntax</a> of the primary algebra of <a href="G._Spencer-Brown" title="G. Spencer-Brown">G. Spencer-Brown</a>'s <i><a href="Laws_of_Form" title="Laws of Form">Laws of Form</a></i>.
</p><p>A <i>basis</i> for <b>2</b> is a set of equations, called <a href="Axiom" title="Axiom">axioms</a>, from which all of the above equations (and more) can be derived. There are many known bases for all Boolean algebras and hence for <b>2</b>. An elegant basis notated using only concatenation and overbar is:
</p>
<ol><li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \ ABC=BCA}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mtext>&nbsp;</mtext>
<mi>A</mi>
<mi>B</mi>
<mi>C</mi>
<mo>=</mo>
<mi>B</mi>
<mi>C</mi>
<mi>A</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \ ABC=BCA}</annotation>
</semantics>
</math></span><img src="./f5efdbffb037b446a9dacf86cdc22c774654dbf2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:14.226ex; height:2.176ex;" alt="{\displaystyle \ ABC=BCA}" loading="lazy"></span> (Concatenation commutes, associates)</li>
<li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\overline {A}}A=1}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>A</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mi>A</mi>
<mo>=</mo>
<mn>1</mn>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\overline {A}}A=1}</annotation>
</semantics>
</math></span><img src="./12e55d8c37cc20c47143c81e139e9fc378f91a24.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.862ex; height:3.009ex;" alt="{\displaystyle {\overline {A}}A=1}" loading="lazy"></span> (<b>2</b> is a <a href="Complement_(order_theory)" class="mw-redirect" title="Complement (order theory)">complemented</a> lattice, with an <a href="Bounded_set" title="Bounded set">upper bound</a> of 1)</li>
<li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \ A0=A}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mtext>&nbsp;</mtext>
<mi>A</mi>
<mn>0</mn>
<mo>=</mo>
<mi>A</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \ A0=A}</annotation>
</semantics>
</math></span><img src="./c14e99f4daeb5527c4de795682e461a0b19debdb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:8.328ex; height:2.176ex;" alt="{\displaystyle \ A0=A}" loading="lazy"></span> (0 is the <a href="Bounded_set" title="Bounded set">lower bound</a>).</li>
<li><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A{\overline {AB}}=A{\overline {B}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi>A</mi>
<mi>B</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>=</mo>
<mi>A</mi>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>B</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle A{\overline {AB}}=A{\overline {B}}}</annotation>
</semantics>
</math></span><img src="./64e938039bf8247227e059fa1e703ed8f051d3a1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:12.086ex; height:3.009ex;" alt="{\displaystyle A{\overline {AB}}=A{\overline {B}}}" loading="lazy"></span> (<b>2</b> is a <a href="Distributive_lattice" title="Distributive lattice">distributive lattice</a>)</li></ol>
<p>Where concatenation = OR, 1 = true, and 0 = false, or concatenation = AND, 1 = false, and 0 = true. (overbar is negation in both cases.)
</p><p>If 0=1, (1)–(3) are the axioms for an <a href="Abelian_group" title="Abelian group">abelian group</a>.
</p><p>(1) only serves to prove that concatenation commutes and associates. First assume that (1) associates from either the left or the right, then prove commutativity. Then prove association from the other direction. Associativity is simply association from the left and right combined.
</p><p>This basis makes for an easy approach to proof, called "calculation" in <i><a href="Laws_of_Form" title="Laws of Form">Laws of Form</a></i>, that proceeds by simplifying expressions to 0 or 1, by invoking axioms (2)–(4), and the elementary identities <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle AA=A,{\overline {\overline {A}}}=A,1+A=1}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>A</mi>
<mi>A</mi>
<mo>=</mo>
<mi>A</mi>
<mo>,</mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mover>
<mi>A</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
<mo>=</mo>
<mi>A</mi>
<mo>,</mo>
<mn>1</mn>
<mo>+</mo>
<mi>A</mi>
<mo>=</mo>
<mn>1</mn>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle AA=A,{\overline {\overline {A}}}=A,1+A=1}</annotation>
</semantics>
</math></span><img src="./71ea6b750ff15db730377f002e59d3d1e01357f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:27.217ex; height:4.176ex;" alt="{\displaystyle AA=A,{\overline {\overline {A}}}=A,1+A=1}" loading="lazy"></span>, and the distributive law.
</p>
<div class="mw-heading mw-heading2"><h2 id="Metatheory">Metatheory</h2></div>
<p><a href="De_Morgan's_theorem" class="mw-redirect" title="De Morgan's theorem">De Morgan's theorem</a> states that if one does the following, in the given order, to any <a href="Boolean_function" title="Boolean function">Boolean function</a>:
</p>
<ul><li>Complement every variable;</li>
<li>Swap '+' and '∙' operators (taking care to add brackets to ensure the order of operations remains the same);</li>
<li>Complement the result,</li></ul>
<p>the result is <a href="Logical_equivalence" title="Logical equivalence">logically equivalent</a> to what you started with. Repeated application of De Morgan's theorem to parts of a function can be used to drive all complements down to the individual variables.
</p><p>A powerful and nontrivial <a href="Metatheorem" title="Metatheorem">metatheorem</a> states that any identity of <b>2</b> holds for all Boolean algebras.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Conversely, an identity that holds for an arbitrary nontrivial Boolean algebra also holds in <b>2</b>. Hence all identities of Boolean algebra are captured by <b>2</b>. This theorem is useful because any equation in <b>2</b> can be verified by a <a href="Decision_procedure" class="mw-redirect" title="Decision procedure">decision procedure</a>. Logicians refer to this fact as "<b>2</b> is <a href="Decidability_(logic)" title="Decidability (logic)">decidable</a>". All known <a href="Decision_procedure" class="mw-redirect" title="Decision procedure">decision procedures</a> require a number of steps that is an <a href="Exponential_function" title="Exponential function">exponential function</a> of the number of variables <i>N</i> appearing in the equation to be verified. Whether there exists a decision procedure whose steps are a <a href="Polynomial_function" class="mw-redirect" title="Polynomial function">polynomial function</a> of <i>N</i> falls under the <a href="P_%3D_NP" class="mw-redirect" title="P = NP">P&nbsp;=&nbsp;NP</a> conjecture.
</p><p>The above metatheorem does not hold if we consider the validity of more general <a href="First-order_logic" title="First-order logic">first-order logic</a> formulas instead of only atomic positive equalities. As an example consider the formula <span class="texhtml">(<i>x</i> = 0) ∨ (<i>x</i> = 1)</span>. This formula is always true in a two-element Boolean algebra. In a four-element Boolean algebra whose domain is the powerset of <span class="nowrap">⁠<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{0,1\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">{</mo>
<mn>0</mn>
<mo>,</mo>
<mn>1</mn>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \{0,1\}}</annotation>
</semantics>
</math></span><img src="./28de5781698336d21c9c560fb1cbb3fb406923eb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.684ex; height:2.843ex;" alt="{\displaystyle \{0,1\}}" loading="lazy"></span>⁠</span>, this formula corresponds to the statement <span class="texhtml">(<i>x</i> = ∅) ∨ (<i>x</i> = {0,1})</span> and is false when <i>x</i> is <span class="nowrap">⁠<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{1\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo fence="false" stretchy="false">{</mo>
<mn>1</mn>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \{1\}}</annotation>
</semantics>
</math></span><img src="./5acdcac635f883f8b4f0a01aa03b16b22f23b124.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:3.487ex; height:2.843ex;" alt="{\displaystyle \{1\}}" loading="lazy"></span>⁠</span>. The decidability for the <a href="First-order_theory" class="mw-redirect" title="First-order theory">first-order theory</a> of many classes of <a href="Boolean_algebras" class="mw-redirect" title="Boolean algebras">Boolean algebras</a> can still be shown, using <a href="Quantifier_elimination" title="Quantifier elimination">quantifier elimination</a> or small model property (with the domain size computed as a function of the formula and generally larger than 2).
</p>
<div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2></div>
<ul><li><a href="Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li>
<li><a href="Bounded_set" title="Bounded set">Bounded set</a></li>
<li><a href="Lattice_(order)" title="Lattice (order)">Lattice (order)</a></li>
<li><a href="Order_theory" title="Order theory">Order theory</a></li></ul>
<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>
<style data-mw-deduplicate="TemplateStyles:r1239543626">
/* start https://en.wikipedia.org/ */


.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}


/* end https://en.wikipedia.org/ */
</style><div class="reflist">
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">
/* start https://en.wikipedia.org/ */


.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}


/* end https://en.wikipedia.org/ */
</style><cite id="CITEREFHalmosGivant2009" class="citation book cs1">Halmos, Paul; Givant, Steven (2009). <i>Introduction to Boolean Algebras</i>. Undergraduate Texts in Mathematics. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-0-387-68436-9">10.1007/978-0-387-68436-9</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a>&nbsp;<bdi>978-0-387-40293-2</bdi>.</cite></span>
</li>
</ol></div></div>
<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>
<p>Many elementary texts on Boolean algebra were published in the early years of the computer era. Perhaps the best of the lot, and one still in print, is:
</p>
<ul><li>Mendelson, Elliot, 1970. <i>Schaum's Outline of Boolean Algebra</i>. McGraw–Hill.</li></ul>
<p>The following items reveal how the two-element Boolean algebra is mathematically nontrivial.
</p>
<ul><li><a href="Stanford_Encyclopedia_of_Philosophy" title="Stanford Encyclopedia of Philosophy">Stanford Encyclopedia of Philosophy</a>: "<a rel="nofollow" class="external text" href="http://plato.stanford.edu/entries/boolalg-math/">The Mathematics of Boolean Algebra</a>," by J. Donald Monk.</li>
<li>Burris, Stanley N., and H.P. Sankappanavar, H. P., 1981. <i><a rel="nofollow" class="external text" href="http://www.thoralf.uwaterloo.ca/htdocs/ualg.html">A Course in Universal Algebra.</a></i> Springer-Verlag. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a>&nbsp;<bdi>3-540-90578-2</bdi>.</li></ul></div><!--htdig_noindex--><div><div class="zim-footer">
This article is issued from <a class="external text" title="Last edited on 2025-04-14" href="https://en.wikipedia.org/wiki/?title=Two-element_Boolean_algebra&amp;oldid=1285567631">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>

</body></html>